#!/usr/bin/ruby -w

require "test/unit"
require "cnf.rb"

class TestCnf < Test::Unit::TestCase

  def test_simple_example
    cnf = CnfFormula.new([CnfClause.new([1])])
    assert_equal("p cnf 1 1\n" +
      "1\n", cnf.to_s)
  end

  def test_example_from_satlib_website
    clause1 = CnfClause.new([1, 3, -4])
    clause2 = CnfClause.new([4])
    clause3 = CnfClause.new([2, -3])
    cnf = CnfFormula.new([clause1, clause2, clause3])
    
    # Note that the real example uses line breaks at ridiculous points to
    # illustrate that you can use them at any place. But, we assert against
    # a format with a line break after each clause.
    assert_equal("p cnf 4 3\n" +
      "1 3 -4 0\n" +
      "4 0\n" +
      "2 -3\n", cnf.to_s)
  end
end
